package typechecker.ast;

import java.util.List;
import java.util.Map;
import java.util.TreeMap;

import typechecker.Stage;
import typechecker.TypeCheckingException;
import typechecker.ast.term.DataConstructor;
import typechecker.ast.type.ForallType;
import typechecker.ast.type.FunctionType;
import typechecker.ast.type.TypeConstructor;
import typechecker.ast.type.TypeConstructorApplication;
import typechecker.ast.type.TypeExpression;
import typechecker.ast.type.TypeVariable;
import typechecker.walkers.PositivityChecker;

public class InductiveDatatype  extends  TreeMap<DataConstructor, TypeExpression >{
	private static final long serialVersionUID = 4472951789680317579L;
	private TypeConstructor cons; 
	private List<TypeVariable> params;
	
	public InductiveDatatype(TypeConstructor name, List<TypeVariable> params) {
		this.params = params;
		this.cons = name;
		cons.setIdt(this);
	}

	public String preetyPrint(){
		String ret = cons + (params.isEmpty()?"":params.toString()) + ":\n";
		for(Map.Entry<DataConstructor, TypeExpression> constr : entrySet()){
			ret += "\t" + constr.getKey().preetyPrint() + "\t- " + constr.getValue().preetyPrint() + "\n"; 
		}
		ret += "\n";
		return ret;
	}

	@Override
	public TypeExpression put(DataConstructor key, TypeExpression value) {
		key.setIdt(this);
		return super.put(key, value);
	}
	
	/**
	 *  The main function that checks inductive definitions. It uses {@link PositivityChecker} to
	 *  check if the type constructor and it's arguments appear on positive positions.
	 * @param constrType The type to check
	 * @throws TypeCheckingException Throws exception when the checking fails.
	 */
	private void checkConstrType(TypeExpression constrType) throws TypeCheckingException{
		TypeExpression crt = constrType;
		PositivityChecker cpw = new PositivityChecker(cons, params, Stage.TEMPLATE_VAR_NAME);
		
		for(int i=0; i < params.size(); i++){
			ForallType fat = (ForallType) crt;
			crt = fat.getBody();
		}
		
		
		/* Check the form of the type O1 -> O2 -> ... -> d X*/
		while( crt instanceof FunctionType){
			FunctionType fcrt = (FunctionType) crt;
			
			if(!cpw.checkPositivity(fcrt.getSrc(), true)){
				throw new TypeCheckingException("Constructor or it's arguments occur on a non-positive position");
			}
			crt = (fcrt.getDest());
		}

		/* The result must be of the form T X */
		if(!(crt instanceof TypeConstructorApplication)){
			throw new TypeCheckingException("Result type of a constructor has wrong result type!");
		} 
		cpw.checkPositivity(crt, false);
		((TypeConstructorApplication)crt).getCons().setStage(new Stage("i", 1));
	}

	public void checkAndAnnotateDef() throws TypeCheckingException{
		for( DataConstructor dc : this.keySet()){
			TypeExpression te = this.get(dc);
			try{
				checkConstrType(te);
			} catch(TypeCheckingException tex){
				System.err.println("Error when checking data constructor " + dc.preetyPrint());
				System.err.println(tex.getMessage());
			}
		}
	}
	
}


